# Copyright 1999-2004 Gentoo Foundation
# Distributed under the terms of the GNU General Public License v2
# $Header: $

inherit eutils

DESCRIPTION="Why - a multi-language multi-prover verification tool"
HOMEPAGE="http://why.lri.fr/index.en.html"
SRC_URI="http://why.lri.fr/download/${P}.tar.gz"

LICENSE="LGPL"
SLOT="0"
KEYWORDS="x86 sparc"

IUSE="alt-ergo coq cvc3 frama-c gappa pvs simplify"
DEPEND="
    >=dev-lang/ocaml-3.07
    >=dev-ml/lablgtk-2.6.0
    alt-ergo? ( sci-mathematics/alt-ergo )
    coq? ( >=sci-mathematics/coq-7.0 )
    pvs? ( sci-mathematics/pvs )
    gappa? ( sci-mathematics/gappa )
    cvc3? ( sci-libs/cvc3 )
    frama-c? ( sci-mathematics/frama-c )
    simplify? ( sci-mathematics/simplify )
  "
RDEPEND="${DEPEND}"

src_unpack() {
	unpack ${A}
	cd ${S}
	epatch ${FILESDIR}/${P}.patch
}

src_compile() {
	econf || die

	myconf="PVSLIB=/opt/pvs/lib"
	make ${myconf} || die
}

src_install() {
	local FRAMAC_PLUGINDIR=${D}usr/lib/frama-c/plugins
	local myconf="COQLIB=${D}usr/lib/coq \
		PVSLIB=${D}opt/pvs/lib \
		DESTDIR=${D} \
		FRAMAC_PLUGINDIR=${FRAMAC_PLUGINDIR}"
	if use frama-c; then
		mkdir -p ${FRAMAC_PLUGINDIR}
	fi
	make $myconf install || die
}
